0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 12 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 134 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 4 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 MRRProof (⇔, 244 ms)
↳29 QDP
↳30 DependencyGraphProof (⇔, 0 ms)
↳31 TRUE
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
MERGEC_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → U3_GGA(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
MERGEC_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(0, T20), T22)
MERGEC_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → U4_GGA(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
MERGEC_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(s(0), T20), T22)
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_GGA(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → LEQA_IN_GG(T35, T36)
LEQA_IN_GG(s(T41), s(T42)) → U1_GG(T41, T42, leqA_in_gg(T41, T42))
LEQA_IN_GG(s(T41), s(T42)) → LEQA_IN_GG(T41, T42)
U5_GGA(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_GGA(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
U5_GGA(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → MERGEC_IN_GGA(T18, .(s(T36), T20), T22)
MERGEC_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_GGA(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
MERGEC_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → LESSB_IN_GG(T59, T57)
LESSB_IN_GG(s(T67), s(T68)) → U2_GG(T67, T68, lessB_in_gg(T67, T68))
LESSB_IN_GG(s(T67), s(T68)) → LESSB_IN_GG(T67, T68)
U7_GGA(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_GGA(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
U7_GGA(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → MERGEC_IN_GGA(.(T57, T58), T60, T62)
MERGEC_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → U9_GGA(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
MERGEC_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEC_IN_GGA(.(s(0), T75), T77, T79)
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_GGA(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → LESSB_IN_GG(T84, T85)
U10_GGA(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_GGA(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U10_GGA(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → MERGEC_IN_GGA(.(s(T85), T75), T77, T79)
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
MERGEC_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → U3_GGA(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
MERGEC_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(0, T20), T22)
MERGEC_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → U4_GGA(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
MERGEC_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(s(0), T20), T22)
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_GGA(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → LEQA_IN_GG(T35, T36)
LEQA_IN_GG(s(T41), s(T42)) → U1_GG(T41, T42, leqA_in_gg(T41, T42))
LEQA_IN_GG(s(T41), s(T42)) → LEQA_IN_GG(T41, T42)
U5_GGA(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_GGA(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
U5_GGA(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → MERGEC_IN_GGA(T18, .(s(T36), T20), T22)
MERGEC_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_GGA(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
MERGEC_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → LESSB_IN_GG(T59, T57)
LESSB_IN_GG(s(T67), s(T68)) → U2_GG(T67, T68, lessB_in_gg(T67, T68))
LESSB_IN_GG(s(T67), s(T68)) → LESSB_IN_GG(T67, T68)
U7_GGA(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_GGA(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
U7_GGA(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → MERGEC_IN_GGA(.(T57, T58), T60, T62)
MERGEC_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → U9_GGA(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
MERGEC_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEC_IN_GGA(.(s(0), T75), T77, T79)
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_GGA(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → LESSB_IN_GG(T84, T85)
U10_GGA(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_GGA(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U10_GGA(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → MERGEC_IN_GGA(.(s(T85), T75), T77, T79)
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
LESSB_IN_GG(s(T67), s(T68)) → LESSB_IN_GG(T67, T68)
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
LESSB_IN_GG(s(T67), s(T68)) → LESSB_IN_GG(T67, T68)
LESSB_IN_GG(s(T67), s(T68)) → LESSB_IN_GG(T67, T68)
From the DPs we obtained the following set of size-change graphs:
LEQA_IN_GG(s(T41), s(T42)) → LEQA_IN_GG(T41, T42)
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
LEQA_IN_GG(s(T41), s(T42)) → LEQA_IN_GG(T41, T42)
LEQA_IN_GG(s(T41), s(T42)) → LEQA_IN_GG(T41, T42)
From the DPs we obtained the following set of size-change graphs:
MERGEC_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_GGA(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
U7_GGA(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → MERGEC_IN_GGA(.(T57, T58), T60, T62)
MERGEC_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(0, T20), T22)
MERGEC_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEC_IN_GGA(.(s(0), T75), T77, T79)
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_GGA(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
U5_GGA(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → MERGEC_IN_GGA(T18, .(s(T36), T20), T22)
MERGEC_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(s(0), T20), T22)
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_GGA(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_GGA(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → MERGEC_IN_GGA(.(s(T85), T75), T77, T79)
mergeC_in_gga([], T5, T5) → mergeC_out_gga([], T5, T5)
mergeC_in_gga([], [], []) → mergeC_out_gga([], [], [])
mergeC_in_gga(T7, [], T7) → mergeC_out_gga(T7, [], T7)
mergeC_in_gga(.(0, T18), .(0, T20), .(0, T22)) → U3_gga(T18, T20, T22, mergeC_in_gga(T18, .(0, T20), T22))
mergeC_in_gga(.(0, T18), .(s(0), T20), .(0, T22)) → U4_gga(T18, T20, T22, mergeC_in_gga(T18, .(s(0), T20), T22))
mergeC_in_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_gga(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U5_gga(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → U6_gga(T35, T18, T36, T20, T22, mergeC_in_gga(T18, .(s(T36), T20), T22))
mergeC_in_gga(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_gga(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U7_gga(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → U8_gga(T57, T58, T59, T60, T62, mergeC_in_gga(.(T57, T58), T60, T62))
mergeC_in_gga(.(s(0), T75), .(0, T77), .(0, T79)) → U9_gga(T75, T77, T79, mergeC_in_gga(.(s(0), T75), T77, T79))
mergeC_in_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_gga(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U10_gga(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → U11_gga(T85, T75, T84, T77, T79, mergeC_in_gga(.(s(T85), T75), T77, T79))
U11_gga(T85, T75, T84, T77, T79, mergeC_out_gga(.(s(T85), T75), T77, T79)) → mergeC_out_gga(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79))
U9_gga(T75, T77, T79, mergeC_out_gga(.(s(0), T75), T77, T79)) → mergeC_out_gga(.(s(0), T75), .(0, T77), .(0, T79))
U8_gga(T57, T58, T59, T60, T62, mergeC_out_gga(.(T57, T58), T60, T62)) → mergeC_out_gga(.(T57, T58), .(T59, T60), .(T59, T62))
U6_gga(T35, T18, T36, T20, T22, mergeC_out_gga(T18, .(s(T36), T20), T22)) → mergeC_out_gga(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22))
U4_gga(T18, T20, T22, mergeC_out_gga(T18, .(s(0), T20), T22)) → mergeC_out_gga(.(0, T18), .(s(0), T20), .(0, T22))
U3_gga(T18, T20, T22, mergeC_out_gga(T18, .(0, T20), T22)) → mergeC_out_gga(.(0, T18), .(0, T20), .(0, T22))
MERGEC_IN_GGA(.(T57, T58), .(T59, T60), .(T59, T62)) → U7_GGA(T57, T58, T59, T60, T62, lessB_in_gg(T59, T57))
U7_GGA(T57, T58, T59, T60, T62, lessB_out_gg(T59, T57)) → MERGEC_IN_GGA(.(T57, T58), T60, T62)
MERGEC_IN_GGA(.(0, T18), .(0, T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(0, T20), T22)
MERGEC_IN_GGA(.(s(0), T75), .(0, T77), .(0, T79)) → MERGEC_IN_GGA(.(s(0), T75), T77, T79)
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20), .(s(T35), T22)) → U5_GGA(T35, T18, T36, T20, T22, leqA_in_gg(T35, T36))
U5_GGA(T35, T18, T36, T20, T22, leqA_out_gg(T35, T36)) → MERGEC_IN_GGA(T18, .(s(T36), T20), T22)
MERGEC_IN_GGA(.(0, T18), .(s(0), T20), .(0, T22)) → MERGEC_IN_GGA(T18, .(s(0), T20), T22)
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77), .(s(T84), T79)) → U10_GGA(T85, T75, T84, T77, T79, lessB_in_gg(T84, T85))
U10_GGA(T85, T75, T84, T77, T79, lessB_out_gg(T84, T85)) → MERGEC_IN_GGA(.(s(T85), T75), T77, T79)
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
MERGEC_IN_GGA(.(T57, T58), .(T59, T60)) → U7_GGA(T57, T58, T59, T60, lessB_in_gg(T59, T57))
U7_GGA(T57, T58, T59, T60, lessB_out_gg(T59, T57)) → MERGEC_IN_GGA(.(T57, T58), T60)
MERGEC_IN_GGA(.(0, T18), .(0, T20)) → MERGEC_IN_GGA(T18, .(0, T20))
MERGEC_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEC_IN_GGA(.(s(0), T75), T77)
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20)) → U5_GGA(T35, T18, T36, T20, leqA_in_gg(T35, T36))
U5_GGA(T35, T18, T36, T20, leqA_out_gg(T35, T36)) → MERGEC_IN_GGA(T18, .(s(T36), T20))
MERGEC_IN_GGA(.(0, T18), .(s(0), T20)) → MERGEC_IN_GGA(T18, .(s(0), T20))
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77)) → U10_GGA(T85, T75, T84, T77, lessB_in_gg(T84, T85))
U10_GGA(T85, T75, T84, T77, lessB_out_gg(T84, T85)) → MERGEC_IN_GGA(.(s(T85), T75), T77)
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
lessB_in_gg(x0, x1)
leqA_in_gg(x0, x1)
U2_gg(x0, x1, x2)
U1_gg(x0, x1, x2)
MERGEC_IN_GGA(.(T57, T58), .(T59, T60)) → U7_GGA(T57, T58, T59, T60, lessB_in_gg(T59, T57))
U7_GGA(T57, T58, T59, T60, lessB_out_gg(T59, T57)) → MERGEC_IN_GGA(.(T57, T58), T60)
MERGEC_IN_GGA(.(0, T18), .(0, T20)) → MERGEC_IN_GGA(T18, .(0, T20))
MERGEC_IN_GGA(.(s(0), T75), .(0, T77)) → MERGEC_IN_GGA(.(s(0), T75), T77)
MERGEC_IN_GGA(.(s(T35), T18), .(s(T36), T20)) → U5_GGA(T35, T18, T36, T20, leqA_in_gg(T35, T36))
MERGEC_IN_GGA(.(0, T18), .(s(0), T20)) → MERGEC_IN_GGA(T18, .(s(0), T20))
MERGEC_IN_GGA(.(s(T85), T75), .(s(T84), T77)) → U10_GGA(T85, T75, T84, T77, lessB_in_gg(T84, T85))
U10_GGA(T85, T75, T84, T77, lessB_out_gg(T84, T85)) → MERGEC_IN_GGA(.(s(T85), T75), T77)
POL(.(x1, x2)) = 2 + 2·x1 + 2·x2
POL(0) = 0
POL(MERGEC_IN_GGA(x1, x2)) = x1 + x2
POL(U10_GGA(x1, x2, x3, x4, x5)) = 1 + 2·x1 + 2·x2 + x3 + 2·x4 + 2·x5
POL(U1_gg(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U2_gg(x1, x2, x3)) = x1 + x2 + x3
POL(U5_GGA(x1, x2, x3, x4, x5)) = 1 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + x5
POL(U7_GGA(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + x3 + x4 + x5
POL(leqA_in_gg(x1, x2)) = 1 + 2·x1 + 2·x2
POL(leqA_out_gg(x1, x2)) = 1 + x1 + 2·x2
POL(lessB_in_gg(x1, x2)) = 1 + x1 + x2
POL(lessB_out_gg(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = 2·x1
U5_GGA(T35, T18, T36, T20, leqA_out_gg(T35, T36)) → MERGEC_IN_GGA(T18, .(s(T36), T20))
lessB_in_gg(0, s(0)) → lessB_out_gg(0, s(0))
lessB_in_gg(s(T67), s(T68)) → U2_gg(T67, T68, lessB_in_gg(T67, T68))
leqA_in_gg(0, 0) → leqA_out_gg(0, 0)
leqA_in_gg(0, s(0)) → leqA_out_gg(0, s(0))
leqA_in_gg(s(T41), s(T42)) → U1_gg(T41, T42, leqA_in_gg(T41, T42))
U2_gg(T67, T68, lessB_out_gg(T67, T68)) → lessB_out_gg(s(T67), s(T68))
U1_gg(T41, T42, leqA_out_gg(T41, T42)) → leqA_out_gg(s(T41), s(T42))
lessB_in_gg(x0, x1)
leqA_in_gg(x0, x1)
U2_gg(x0, x1, x2)
U1_gg(x0, x1, x2)